1. Field of the Invention
Embodiments of the invention relate to the field of electronic design automation (EDA), and more specifically, to equivalence checking.
2. Description of Related Art
Equivalence checking has become important in many design synthesis and optimization tools. In equivalence checking, an implementation circuit is compared with a reference circuit to determine if the two circuits are functionally equivalent. There are a number of techniques in equivalence checking: functional, automatic test pattern generation (ATPG), and incremental. Functional approaches use Binary Decision Diagrams (BDD's) to compare the two circuits. The circuits are equivalent if and only if their corresponding BDD's are isomorphic. ATPG approaches prove the equivalence of the two circuits under verification by proving that the stuck-at-0 is a redundant fault for their miter output. A variation of the ATPG is the Boolean Satisfiability (SAT) technique. Incremental approaches are based on reducing the miter circuit through the identification of internal equivalent pairs of the circuit nodes. Among these techniques, those using BDD's are popular.
The use of BDD's has a number of problems. First, if the circuit (or its subcircuits) are complex, their BDD's may become quite large, exceeding allocated storage and leading to high processing time. Second, false negatives may result. A false negative is a problem in which the two circuits are equivalent but the equivalence checker or verifier declares them as different.
Therefore, there is a need to have an efficient technique to improve verification of digital circuits.